package rdp;

import java.util.ArrayList;
import java.util.Arrays;

import systeme.GrapheRdP;
/**
 * Classe permettant de faire les verifications en arriere. On travaille sur les etats predecesseurs.
 * Implementer les algorithmes vus en cours
 * Certaines méthodes fonctionnent de la meme maniere que dans la classe CTL.
 */
public class CTLArriere {
	
	GrapheRdP g_rdp;
	
	public CTLArriere(GrapheRdP g_rdp) {
		this.g_rdp=g_rdp;
	}

	//Ne change pas par rapport a CTL
	/**
	 * Pour une place donnée, est ce que dans les différents etats du GrapheRdp cette place est marquée ?
	 * @param i la place dont on veut savoir si elle est marquée
	 * @return un tableau de booleens ex : 110 si c'est la propriete est vraie dans l'etat et l'etat 2
	 */
	public boolean[] prop(int i) {

		boolean[] res=new boolean[g_rdp.etat.size()];
		Arrays.fill(res,false);
		//Pour chaque etat
		for(int j=0; j<g_rdp.etat.size();j++){
			//Si la place i est marquée dans cet etat
			if(g_rdp.etat.get(j)[i]){
				res[j]=true;
			}
		}
		return res;
	}

	//Ne change pas par rapport a CTL
	public boolean[] faux() {
		boolean[] res = new boolean[g_rdp.succ.size()];
		Arrays.fill(res,false);
		return res;
	}

	//Ne change pas par rapport a CTL
	public boolean[] vrai() {
		boolean[] res = new boolean[g_rdp.succ.size()];
		Arrays.fill(res,true);
		return res;
	}

	//Ne change pas par rapport a CTL
	public boolean[] neg(boolean[] etatsVerifiantFormuleA) {
		boolean[] res = new boolean[g_rdp.succ.size()];
		for (int i=0; i<g_rdp.succ.size(); i++)
			res[i] = !etatsVerifiantFormuleA[i];
		return res;
	}
	//Ne change pas par rapport a CTL
	public boolean[] or(boolean[] etatsVerifiantFormuleA, boolean[] etatsVerifiantFormuleB) {
		boolean[] res = new boolean[g_rdp.succ.size()];
		for (int i=0; i<g_rdp.succ.size(); i++)
			res[i] = etatsVerifiantFormuleA[i] || etatsVerifiantFormuleB[i];
		return res;
	}
	//Ne change pas par rapport a CTL
	public boolean[] and(boolean[] etatsVerifiantFormuleA, boolean[] etatsVerifiantFormuleB) {
		boolean[] res = new boolean[g_rdp.succ.size()];
		for (int i=0; i<g_rdp.succ.size(); i++)
			res[i] = etatsVerifiantFormuleA[i] && etatsVerifiantFormuleB[i];
		return res;
	}

	/**
	 * Par definition Ax signifie qu'il existe un fils qui vérifie la propriete
	 * Implementer l'algorithme vu en cours :
	 * res recois l'ensemble vide
	 * pour tout etat s verifiant la formule f : res recois res Union pred(s)
	 * 
	 * @param etatsVerifiantFormule : le tableau des etats ou la formule f est vraie
	 * @return
	 */
	public boolean[] EX(boolean[] etatsVerifiantFormule) {
		boolean[] res = new boolean[g_rdp.pred.size()];
		//pour tout etat
		for (int i=0; i<g_rdp.pred.size(); i++) {
			res[i] = false;
			//si cet etat verifie la formule
			if(etatsVerifiantFormule[i]){
				//trouver les predecesseurs de i
				ArrayList<Integer> predecesseurs=g_rdp.pred.get(i);
				for(int indicePred=0; indicePred<predecesseurs.size(); indicePred++){
					res[predecesseurs.get(indicePred)]=true;
				}
			}

		}
		return res;
	}

	/**
	 * Par definition Ax signifie que tous les fils vérifient la propriete
	 * Implementer l'algorithme vu en cours :
	 * utiliser un tableau res, initialisé au nombre de successeurs.
	 * si 0 a 3 successeurs et 1 a 2 successeurs, res = [3,2]
	 * Pour chaque état verifiant f,
	 * res=res -pred(s)
	 * Parcourir res, si res[i] vaut 0 alors i verifie Ax(f)
	 * 
	 * @param etatsVerifiantsFormule : le tableau des etats ou la formule f est vraie
	 * @return le tableau des etats qui verifient Ax(f)
	 */
	public boolean[] AX(boolean[] etatsVerifiantsFormule) {
		boolean [] res=new boolean[g_rdp.etat.size()];
		//Init compteursSuccesseurs, ce tableau contient le nombre d'etats successeurs qui ne verifient pas f.
		// <--> Si compteursSuccesseurs[i] == 0 alors cela veut dire que tout les successeurs verifient f
		int [] compteursSuccesseurs=new int[g_rdp.etat.size()];
		for(int i=0;i<g_rdp.etat.size(); i++){
			compteursSuccesseurs[i]=g_rdp.succ.get(i).size();
		}
		for(int j=0; j<g_rdp.etat.size(); j++){
			//Si cet état verifie la formule f
			if(etatsVerifiantsFormule[j]){
				//recuperer les predecesseur de cet etat
				ArrayList<Integer> predecesseurs=g_rdp.pred.get(j);
				//Pour chaque etat predecesseur,
				for(int indicePredecesseur=0; indicePredecesseur<predecesseurs.size(); indicePredecesseur++){
					//Décrémenter le nombre de successeurs qui ne verifient pas f
					compteursSuccesseurs[predecesseurs.get(indicePredecesseur)]-=1;
				}
			}
		}
		return res;
	} 

	public boolean[] EU(boolean[] etatsVerifiantFormuleA, boolean[] etatsVerifiantFormuleB) {
		boolean[] res = faux();
		boolean[] avant;
		do {
			avant = res;
			res = or(etatsVerifiantFormuleB,and(etatsVerifiantFormuleA,EX(res)));
		} 
		while(!Arrays.equals(avant,res));
		return res;
	}

	public boolean[] AU(boolean[] etatsVerifiantFormuleA, boolean[] etatsVerifiantFormuleB) {
		boolean[] res = faux();
		boolean[] avant;
		do {
			avant = res;
			res = or(etatsVerifiantFormuleB,and(etatsVerifiantFormuleA,AX(res)));
		} 
		while(!Arrays.equals(avant,res));
		return res;
	}
	
}
